On the power of clause-learning SAT solvers as resolution engines
Clause Learning と Restart の組み合わせ (CLR) だと、多項式オーダーに収まるように証明ができあがるという話
Δ と α が論理式で l がリテラルであるとき、Δ から α が導かれるならば$ \Delta \models \alphaと書く。
l が unit resolution を用いることで Δ から導かれるならば $ \Delta \vdash_1 lと書く。
節をリテラルの集合と考え、CNF 式を節の集合と考える。
証明系とは、証明の大きさに対して多項式時間でそれを verify できるような証明を表すための言語のことである。
節 α ∨ x と β ∨ ¬ x の resolution とは、そこから節 α ∨ β (resolvent) が導かれることを指す。
ここで、x のことを resolved variable という。
CNF Δ にある節$ C_kのresolution proof (resolution derivation) とは節の並びのことで、それぞれの節は Δ にあるか、以前に resolvent として導かれたものである。
resolution proof のことを、その中に含まれる節の集合として考えることもある。
empty clause の resolution proof のことを、refutation proof という。
この論文だと、証明系のことを、その系が許容するすべての refutation proof を含む集合であると見ることができる。
CNF Δ が 1-consistent <=>$ \Delta \vdash_1 \texttt{false}
$ \Delta \nvdash_1 \texttt{false} は 1-consistent
CLR state (Δ, Γ, D) が 1-inconsistent <=> Δ ∧ Γ ∧ D が 1-inconsistent
一般に、充足不可能な CNF は 1-consistent
CLR state S = (Δ, Γ, D) のとき、$ \Delta \land \Gamma \land D \vdash_1 lならば$ S \vdash_1 lと書く。
1-consistent だと、unit resolution をしたところでまだ UNSAT であるかわかってないということ？
knowledge base とは $ \Delta \land \Gammaのこと（Γ は conflict clause たちを持った学習節の集合）